(declare-const v0 Bool)
(declare-const r0 Real)
(declare-const r1 Real)
(declare-const r2 Real)
(declare-const r3 Real)
(declare-const v1 Bool)
(assert (forall ((q0 Real)) v1))
(declare-const v2 Bool)
(assert (exists ((q1 Real) (q2 Real) (q3 Bool)) (not (= q3 v0 q3))))
(assert (or (forall ((q1 Real) (q2 Real) (q3 Bool)) (and v2 v0 (= v1 v0 v0 v0 v1 v1) (= v1 v0 v0 v0 v1 v1) v0 v0 (= v1 v0 v0 v0 v1 v1) (= r2 r2 r1) v2)) (exists ((q1 Real) (q2 Real) (q3 Bool)) (not (xor v1 q3 (and v2 v0 (= v1 v0 v0 v0 v1 v1) (= v1 v0 v0 v0 v1 v1) v0 v0 (= v1 v0 v0 v0 v1 v1) (= r2 r2 r1) v2) v2 q3 v2 q3 v0 v2 v0 q3)))))
(declare-const r4 Real)
(declare-const v3 Bool)
(declare-const v4 Bool)
(push)
(declare-const v5 Bool)
(declare-const v6 Bool)
(assert (exists ((q4 Real) (q5 Real) (q6 Bool)) (not (distinct q4 r1 q4 r2))))
(push)
(declare-const r5 Real)
(declare-const v7 Bool)
(pop)
(push)
(push)
(assert (not (forall ((q7 Real)) (and (distinct 0.0 0.0 0.0 r1 r1) v4 (and v2 v0 (= v1 v0 v0 v0 v1 v1) (= v1 v0 v0 v0 v1 v1) v0 v0 (= v1 v0 v0 v0 v1 v1) (= r2 r2 r1) v2) (distinct 0.0 0.0 0.0 r1 r1) (> r1 (- r1) 0.0 r3) (= v1 v0 v0 v0 v1 v1) (and v2 (distinct 0.0 0.0 0.0 r1 r1) v2)))))
(assert (or (forall ((q7 Real)) (not (<= (- r2) 925.0 q7 q7 91647.0))) (exists ((q7 Real)) (> r1 (- 0.0 (- r3) (- r2)) (- r1) r3 r4))))
(check-sat)
